{-
 -  Separ, Type/Lattice.hs
 -
 -  Copyright (c) 2010 Dariusz Leniowski. All Rights Reserved.
 -
 -  Redistribution and use in source and binary forms, with or without 
 -  modification, are permitted provided that the following conditions 
 -  are met:
 -
 -  1. Redistributions of source code must retain the above copyright 
 -     notice, this list of conditions and the following disclaimer.
 -
 -  2. Redistributions in binary form must reproduce the above copyright 
 -     notice, this list of conditions and the following disclaimer 
 -     in the documentation and/or other materials provided with 
 -     the distribution.
 -
 -  3. The name of the author may not be used to endorse or promote 
 -     products derived from this software without specific prior 
 -     written permission.
 -
 -  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 
 -  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 
 -  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 
 -  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL 
 -  THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, 
 -  INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES 
 -  (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS 
 -  OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) 
 -  HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, 
 -  STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING 
 -  IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 
 -  POSSIBILITY OF SUCH DAMAGE.
 -
 -}

{-# LANGUAGE FlexibleContexts #-}

-- Module Lattice
-- class-lattice functions which are not automatically generated and depend on the data
--   (clsLeq, clsLca, clsGcd, clsFsg, clsGsf, etc.)
-- type-lattice functions (lca, gcd)
-- evalProperty (here because of dependencies (again :-[))

module Type.Lattice where

import Prelude hiding (gcd)
import Control.Monad hiding (ap)

import Data.Bits as Bits

import Type.Base
import Type.ClsType
import Type.ClsData hiding (t)

clsIsNotE :: ClsType -> Bool
clsIsNotE (C 0 0) = error $ "illegal class: (C 0 0)"
clsIsNotE (C _ 0) = True
clsIsNotE (C 0 _) = False

-- classes equality
clsEq :: ClsType -> ClsType -> Bool
clsEq a b = a == b

-- LEQ = isSubclassOf
-- Int <: Number
clsLeq :: ClsType -> ClsType -> Bool
clsLeq a b = clsIsSubclassOf a b

-- LCA (max)
-- Number = LCA(Int, Float)
clsLca :: ClsType -> ClsType -> ClsType
clsLca (C 0 0) (C 0 0) = 
	error $ "illegal classes: (C 0 0) (C 0 0)"
clsLca (C 0 0) _ = error $ "illegal class: (C 0 0)"
clsLca _ (C 0 0) = error $ "illegal class: (C 0 0)"
clsLca (C 1 0) (C _ 0)  = (C 1 0) -- TODO should I do this by guards?
clsLca (C _ 0) (C 1 0) = (C 1 0)
clsLca (C 2 0) (C i2 0) = (C i2 0)
clsLca (C i1 0) (C 2 0) = (C i1 0)
clsLca (C 3 0) (C 4 0) = (C 1 0)
clsLca (C 4 0) (C 3 0) = (C 1 0)
clsLca (C i1 0) (C i2 0) = 
	let e1 = clsIToE i1 in 
	let e2 = clsIToE i2 in
	clsEToCls (e1 .&. e2)
clsLca (C i1 0) (C 0 e2) = let e1 = clsIToE i1 in clsEToCls (e1 .&. e2)
clsLca (C 0 e1) (C i2 0) = let e2 = clsIToE i2 in clsEToCls (e1 .&. e2)
clsLca (C 0 e1) (C 0 e2) = clsEToCls (e1 .&. e2)
clsLca c1@(C _ _) c2@(C _ _) = 
	error $ "illegal classes: " ++ show c1 ++ " and " ++ show c2

-- GCD (min)
-- dual of LCA
clsGcd :: ClsType -> ClsType -> ClsType
clsGcd (C 0 0) (C 0 0) = 
	error $ "illegal classes: (C 0 0) (C 0 0)"
clsGcd (C 0 0) _ = error $ "illegal class: (C 0 0)"
clsGcd _ (C 0 0) = error $ "illegal class: (C 0 0)"
clsGcd (C 1 0) (C i2 0) = (C i2 0) -- TODO should I do this by guards?
clsGcd (C i1 0) (C 1 0) = (C i1 0)
clsGcd (C 2 0) (C _ 0) = (C 2 0)
clsGcd (C _ 0) (C 2 0) = (C 2 0)
clsGcd (C 3 0) (C 4 0) = (C 2 0)
clsGcd (C 4 0) (C 3 0) = (C 2 0)
clsGcd (C i1 0) (C i2 0) = 
	let e1 = clsIToE i1 in 
	let e2 = clsIToE i2 in
	clsEToCls (e1 .|. e2)
clsGcd (C i1 0) (C 0 e2) = let e1 = clsIToE i1 in clsEToCls (e1 .|. e2)
clsGcd (C 0 e1) (C i2 0) = let e2 = clsIToE i2 in clsEToCls (e1 .|. e2)
clsGcd (C 0 e1) (C 0 e2) = clsEToCls (e1 .|. e2)
clsGcd c1@(C _ _) c2@(C _ _) = 
	error $ "illegal classes: " ++ show c1 ++ " and " ++ show c2

-- fsg a b :> x <=> a :> b | x
-- cc = aa .&. (complement bb)
clsFsg :: ClsType -> ClsType -> ClsType
clsFsg (C 0 e1) (C 0 e2) = 
	let e3 = e1 .&. complement e2 in -- e1 >= 0, so e2 >= 0
	let f e i = 
		if testBit e (clsIBit i) then e .|. (clsIToE i) 
		else e
	in clsEToCls $ foldl f e3 $ drop clsNSpecial clsGetAllI
clsFsg (C i1 0) (C i2 0) = clsFsg (C 0 (clsIToE i1)) (C 0 (clsIToE i2))
clsFsg (C i1 0) c2 = clsFsg (C 0 (clsIToE i1)) c2
clsFsg c1 (C i2 0) = clsFsg c1 (C 0 (clsIToE i2))
clsFsg c1@(C _ _) c2@(C _ _) = 
	error $ "illegal classes: " ++ show c1 ++ " and " ++ show c2

-- x :> gsf a b <=> b & x :> a
-- cc = aa .|. (complement bb)
clsGsf :: ClsType -> ClsType -> ClsType
clsGsf (C 0 e1) (C 0 e2) = 
	let e3 = (e1 .|. complement e2) .&. (clsIToE clsNothingI) in
	let f e i =	
		let ei = clsIToE i in
		if ei .&. e == ei then e
		else clearBit e (clsIBit i)
	in clsEToCls $ foldl f e3 $ drop clsNSpecial clsGetAllI
clsGsf (C i1 0) (C i2 0) = clsGsf (C 0 (clsIToE i1)) (C 0 (clsIToE i2))
clsGsf (C i1 0) c2 = clsGsf (C 0 (clsIToE i1)) c2
clsGsf c1 (C i2 0) = clsGsf c1 (C 0 (clsIToE i2))
clsGsf c1@(C _ _) c2@(C _ _) = 
	error $ "illegal classes: " ++ show c1 ++ " and " ++ show c2

-----------------------------------------------
-- LCA, GCD
-----------------------------------------------

-- Least Common Ancestor (Max)
-- The farthest concept from the root which is 
-- a super-concept of both a and b.
-- Number = LCA(Int, Float)
lca :: (Evaluable Type, Lambdable Type, Quantifiable Type) => Type -> Type -> MM Type

lca = lca' True

-- this is an ugly hack
-- first argument True means expand class
-- it is set to False when in property
-- it is set to True again when in function
lca' :: (Evaluable Type, Lambdable Type, Quantifiable Type) => Bool -> Type -> Type -> MM Type
lca' _ (Cls c) _ | clsIsThing c = return typeThing
lca' _ (Cls c) b | clsIsNothing c = return b
lca' _ _ (Cls c) | clsIsThing c = return typeThing
lca' _ b (Cls c) | clsIsNothing c = return b
lca' _ a@(App _ _ _) b = return $ Lca a b
lca' _ a b@(App _ _ _) = return $ Lca a b
lca' e a@(Var _ _ _ _) b = do
	(t,i) <- unquantify False a
	lca' e t b >>= quantify i
lca' e a b@(Var _ _ _ _) = do
	(t,i) <- unquantify False b
	lca' e a t >>= quantify i
lca' e a@(Ref r) b = 
		isVarFree r >>= choice 
		(return $ Lca a b)
		(getVarValue r >>= lca' e b)
lca' e a b@(Ref r) = 
		isVarFree r >>= choice 
		(return $ Lca a b)
		(getVarValue r >>= lca' e a)
lca' e (PSet at n av) b = do
	(bt,bv) <- popProperty n b
	v' <- lca' False av bv
	t' <- lca' e at bt
	return $ pSet t' n v'
lca' e a b@(PSet _ _ _) = lca' e b a
lca' e (PGet t "self") b = evalProperty "self" t >>= lca' False b
lca' e (PGet t n) b = evalProperty n t >>= lca' e b
lca' e a b@(PGet _ _) = lca' e b a
lca' _ (Lam b1 a1 r1) (Lam b2 a2 r2) = 
	if b1 == b2 then 
		liftM2 (Lam b1) (gcd a1 a2) (lca' True r1 r2)
	else return typeThing
lca' e a@(Lam b1 _ _) b =
	inCase (return typeThing) $ do
		(a2,r2,i) <- makeLam False b1 b
		lca' e a (Lam b1 a2 r2) >>= quantify i
lca' e a b@(Lam _ _ _) = lca' e b a
lca' e a@(Lca a1 a2) b@(Lca b1 b2) = do
	a' <- lca' e a1 a2
	b' <- lca' e b1 b2
	case (a',b') of
		(Lca _ _, Lca _ _) -> return $ Lca a' b'
		_ -> lca' e a' b'
lca' e a@(Lca a1 a2) b = do
	a' <- lca' e a1 a2
	case a' of
		(Lca _ _) -> return (Lca a' b) -- TODO try Lca a2 b a1 first
		_ -> lca' e a' b
lca' e a b@(Lca _ _) = lca' e b a	
lca' e (Gcd a1 a2) b = do
	c1 <- gcd a1 a2
	case c1 of
		(Gcd _ _) -> return $ Lca c1 b
		_ -> lca' e c1 b
lca' e a b@(Gcd _ _) = lca' e b a
lca' e (Cls a) (Cls b) | clsIsNothingThing a = return $ Cls $ clsLca a b -- TODO this is ugly
lca' e (Cls a) (Cls b) | clsIsNothingThing b = return $ Cls $ clsLca a b
lca' e (Cls a) b | clsIsNothingThing a = return b -- TODO this is even worse
lca' e a (Cls b) | clsIsNothingThing b = return a
lca' True (Cls a) (Cls b) = 
	(return $ Cls $ clsLca a b) 
		-- TODO this should be enforced by the ontology
		-- but it feels somehow wrong, it is a computer job
		-- to check and complete that kind of things, isn't it?
		-- `mplus` (do
		-- ta <- clsGetSubtype a (Cls a)
		-- tb <- clsGetSubtype b (Cls b)
		-- lca' True ta tb)
lca' False (Cls a) (Cls b) = return $ Cls $ clsLca a b
-- TODO remove following two lines
--lca' e (Cls c) b = clsGetSubtype c (Cls c) >>= lca' e b
--lca' e a (Cls c) = clsGetSubtype c (Cls c) >>= lca' e a

-- Greatest Common Descendant
-- Dual of LCA (Min)
gcd :: (Evaluable Type, Lambdable Type, Quantifiable Type) => Type -> Type -> MM Type
gcd = gcd' True

-- this is an ugly hack
-- first argument True means expand class
-- it is set to False when in property
-- it is set to True again when in function
gcd' :: (Evaluable Type, Lambdable Type, Quantifiable Type) => Bool -> Type -> Type -> MM Type
gcd' _ (Cls c) _ | clsIsNothing c = return typeNothing
gcd' _ (Cls c) b | clsIsThing c = return b
gcd' _ _ (Cls c) | clsIsNothing c = return typeNothing
gcd' _ b (Cls c) | clsIsThing c = return b
gcd' _ a@(App _ _ _) b = return $ Gcd a b
gcd' _ a b@(App _ _ _) = return $ Gcd a b
gcd' e a@(Var _ _ _ _) b = do
	(t,i) <- unquantify False a
	gcd' e t b >>= quantify i
gcd' e a b@(Var _ _ _ _) = do
	(t,i) <- unquantify False b
	gcd' e a t >>= quantify i
gcd' e a@(Ref r) b = do
	isVarFree r >>= choice 
		(return $ Gcd a b)
		(getVarValue r >>= gcd' e b)
gcd' e a b@(Ref r) = do
	isVarFree r >>= choice
		(return $ Gcd a b)
		(getVarValue r >>= gcd' e a)
gcd' e (PSet at n av) b = do
	(bt,bv) <- popProperty n b
	v' <- gcd' False av bv
	t' <- gcd' e at bt
	return $ pSet t' n v'
gcd' e a b@(PSet _ _ _) = gcd' e b a	
gcd' e (PGet t "self") b = evalProperty "self" t >>= gcd' False b
gcd' e (PGet t n) b = evalProperty n t >>= gcd' e b
gcd' e a b@(PGet _ _) = gcd' e b a
gcd' e (Lam b1 a1 r1) (Lam b2 a2 r2) = 
	if b1 == b2 then
		liftM2 (Lam b1) (lca a1 a2) (gcd' True r1 r2)
	else return typeNothing
gcd' e a@(Lam b1 _ _) b = 
	inCase (return typeNothing) $ do
		(a2,r2,i) <- makeLam False b1 b 
		gcd' e a (Lam b1 a2 r2) >>= quantify i
gcd' e a b@(Lam _ _ _) = gcd' e b a
gcd' e a@(Gcd a1 a2) b@(Gcd b1 b2) = do
	a' <- gcd' e a1 a2
	b' <- gcd' e b1 b2
	case (a',b') of
		(Gcd _ _, Gcd _ _) -> return (Gcd a' b')
		_ -> gcd' e a' b'
gcd' e a@(Gcd a1 a2) b = do
	a' <- gcd' e a1 a2
	case a' of
		(Gcd _ _) -> return (Gcd a' b) -- TODO try Gcd a2 b a1 first
		_ -> gcd' e a' b
gcd' e a b@(Gcd _ _) = gcd' e b a		
gcd' e (Lca a1 a2) b = do
	c1 <- gcd' e a1 b
	c2 <- gcd' e a2 b
	lca c1 c2
gcd' e a b@(Lca _ _) = gcd' e b a
gcd' e (Cls a) (Cls b) | clsIsNothingThing a = return $ Cls $ clsGcd a b -- TODO ugly as before
gcd' e (Cls a) (Cls b) | clsIsNothingThing b = return $ Cls $ clsGcd a b
gcd' e (Cls a) b | clsIsNothingThing a = return b -- TODO same here
gcd' e a (Cls b) | clsIsNothingThing b = return a
gcd' True (Cls a) (Cls b) = 
	(return $ Cls $ clsGcd a b) 
		-- TODO same as in lca
		-- `mplus` (do
		-- ta <- clsGetSubtype a (Cls a)
		-- tb <- clsGetSubtype b (Cls b)
		-- gcd' True ta tb)
gcd' False (Cls a) (Cls b) = return $ Cls $ clsGcd a b
-- TODO remove following two lines
--gcd' e (Cls c) b = clsGetSubtype c (Cls c) >>= gcd' e b
--gcd' e a (Cls c) = clsGetSubtype c (Cls c) >>= gcd' e a

-------------------------------------------------------
-- Temporary interface for handling class hierarchy
-- cls: LCA, GCD, FSG, GSF
-------------------------------------------------------

-- FSG
-- fsg a b <: x <=> a <: b | x
--
-- a1->a2 <: b1->b2 | x1->x2
-- a1->a2 <: (b1&x1)->(b2|x2)
-- b1 & x1 <: a1, a2 <: b2 | x2
-- x1 <: gsf a1 b1, fsg a2 b2 <: x2
fsg :: (Evaluable Type, Lambdable Type, Quantifiable Type) => Type -> Type -> MM Type
fsg a (Ref r) = do
	isVarFree r >>= choice
		(return $ Cls(C 0 0))
		(getVarValue r >>= fsg a)
fsg (Ref r) b = do
	isVarFree r >>= choice
		(return $ Cls(C 0 0))
		(getVarValue r >>= flip fsg b)
fsg (Cls a) (Cls b) = return $ Cls $ clsFsg a b
fsg (PSet at n av) b = do
	(bt,bv) <- popProperty n b
	v' <- fsg av bv
	t' <- fsg at bt
	return $ pSet t' n v'
fsg a (PSet bt n bv) = do
	(at,av) <- popProperty n a
	v' <- fsg av bv
	t' <- fsg at bt
	return $ pSet t' n v'	
fsg (PGet t n) b = evalProperty n t >>= flip fsg b
fsg a (PGet t n) = evalProperty n t >>= fsg a
fsg (Lam b1 a1 r1) (Lam b2 a2 r2) = 
	if b1 == b2 then 
		liftM2 (Lam b2) (gsf a1 a2) (fsg r1 r2)
	else return $ Cls(C 0 0)
fsg a@(Lam b1 _ _) b = 
	inCase (return $ Cls(C 0 0)) $ do
		(a2,r2,i) <- makeLam False b1 b
		fsg a (Lam b1 a2 r2) >>= quantify i
fsg a b@(Lam b2 _ _) = 
	inCase (return $ Cls(C 0 0)) $ do
		(a1,r1,i) <- makeLam False b2 a
		fsg (Lam b2 a1 r1) b >>= quantify i
-- WARNING HACK :-(
fsg _ _ = return $ Cls(C 0 0) -- TODO should I remove this hack?
	-- this means that fsg couldn't be computed

-- GSF
-- x <: gsf a b <=> b & x <: a
gsf :: (Evaluable Type, Lambdable Type, Quantifiable Type) => Type -> Type -> MM Type
gsf (Cls a) (Cls b) = return $ Cls $ clsGsf a b
gsf a (Ref r) = do
	isVarFree r >>= choice
		(return $ Cls(C 0 0))
		(getVarValue r >>= gsf a)
gsf (Ref r) b = do
	isVarFree r >>= choice
		(return $ Cls(C 0 0))
		(getVarValue r >>= flip gsf b)
gsf (PSet at n av) b = do
	(bt,bv) <- popProperty n b
	v' <- gsf av bv
	t' <- gsf at bt
	return $ pSet t' n v'
gsf a (PSet bt n bv) = do
	(at,av) <- popProperty n a
	v' <- gsf av bv
	t' <- gsf at bt
	return $ pSet t' n v'	
gsf (PGet t n) b = evalProperty n t >>= flip gsf b
gsf a (PGet t n) = evalProperty n t >>= gsf a
gsf (Lam b1 a1 r1) (Lam b2 a2 r2) = 
	if b1 == b2 then 
		liftM2 (Lam b2) (fsg a1 a2) (gsf r1 r2)
	else return $ Cls(C 0 0)
gsf a@(Lam b1 _ _) b = 
	inCase (return $ Cls(C 0 0)) $ do
		(a2,r2,i) <- makeLam False b1 b
		gsf a (Lam b1 a2 r2) >>= quantify i
gsf a b@(Lam b2 _ _) = 
	inCase (return $ Cls(C 0 0)) $ do
		(a1,r1,i) <- makeLam False b2 a 
		gsf (Lam b2 a1 r1) b >>= quantify i
-- WARNING HACK :-(
gsf _ _ = return $ Cls(C 0 0) -- TODO shoud I remove this hack?


-------------------------------------------
-- evalProperty
-- gets property from PSet
-- TODO read property also from classes
-------------------------------------------

evalProperty :: (Evaluable Type, Lambdable Type, Quantifiable Type) => String -> Type -> MM Type
evalProperty name term = evalProperty' name term term

evalProperty' :: (Evaluable Type, Lambdable Type, Quantifiable Type) => String -> Type -> Type -> MM Type
evalProperty' "self" orgt t = return orgt
evalProperty' name orgt (Cls c) | clsIsNothing c = return typeNothing
evalProperty' name orgt (Cls c) | c `clsIsSubclassOf` clsThingNothing = return typeNothing
evalProperty' name orgt (Cls c) = inCase (return typeThing) (clsGetProperty name c orgt)
evalProperty' name orgt (Ref r) = do
	isVar r >>= choice (
		isVarFree r
			>>= choice 
				(liftM snd $ getVarBounds r) 
				(getVarValue r) 
			>>=	evalProperty' name orgt
		) (return typeThing)
evalProperty' name orgt (Lca a b) = do
	a' <- evalProperty' name orgt a
	b' <- evalProperty' name orgt b
	lca a' b'
evalProperty' name orgt (Gcd a b) = do
	a' <- evalProperty' name orgt a
	b' <- evalProperty' name orgt b
	gcd a' b'
evalProperty' name orgt (Lam _ _ r) = evalProperty' name orgt r
evalProperty' name orgt t@(Var _ _ _ _) = do
	(t',i) <- unquantify False t
	evalProperty' name orgt t' >>= quantify i
evalProperty' name orgt t@(App _ _ _) = eval t >>= evalProperty' name orgt
evalProperty' name orgt (PSet _ n v) | n == name = return v
evalProperty' name orgt (PSet t _ _) | otherwise = evalProperty' name orgt t
evalProperty' name orgt (PGet t n) = evalProperty n t >>= evalProperty' name orgt

-------------------------------------------
-- popProperty
-- gets property from PSet like evalProperty,
-- but also removes it from there if present (and possible)
-- TODO read property also from classes
-------------------------------------------

popProperty :: (Evaluable Type, Lambdable Type, Quantifiable Type) => String -> Type -> MM (Type,Type)
popProperty name term = popProperty' name term term

popProperty' :: (Evaluable Type, Lambdable Type, Quantifiable Type) => String -> Type -> Type -> MM (Type,Type)
popProperty' "self" orgt t = return (t,t)
popProperty' name orgt t@(Cls _) = do
	property <- evalProperty' name orgt t
	return (t,property)
popProperty' name orgt t@(Ref _) = do
	property <- evalProperty' name orgt t
	return (t,property)
popProperty' name orgt (Lca a b) = do
	(a',ap) <- popProperty' name orgt a
	(b',bp) <- popProperty' name orgt b
	p <- lca ap bp
	return (Lca a' b', p)
popProperty' name orgt (Gcd a b) = do
	(a',ap) <- popProperty' name orgt a
	(b',bp) <- popProperty' name orgt b
	p <- gcd ap bp
	return (Gcd a' b', p)
popProperty' name orgt (Lam b a r) = do
	(r',p) <- popProperty' name orgt r
	return (Lam b a r', p)
popProperty' name orgt t@(Var _ _ _ _) = do
	(t',i) <- unquantify False t
	(_,p) <- popProperty' name orgt t' 
	p' <- quantify i p
	return (t,p')
popProperty' name orgt t@(App _ _ _) = eval t >>= popProperty' name orgt
popProperty' name orgt (PSet u n v) | n == name = return (u,v)
popProperty' name orgt (PSet u n v) | otherwise = do
	(u',p) <- popProperty' name orgt u
	return (pSet u' n v, p)
popProperty' name orgt (PGet u n) = evalProperty n u >>= popProperty' name orgt

